Nuprl Lemma : namer-disjoint-shift
11,40
postcript
pdf
n
,
m
:
,
nmr
:Namer(
n
+
m
;[]). namer-disjoint(
n
;
m
;
nmr
;namer-shift(
n
;
nmr
))
latex
Definitions
n
+
m
,
a
<
b
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
{
x
:
A
|
B
(
x
)}
,
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
Void
,
x
:
A
B
(
x
)
,
t
T
,
x
:
A
B
(
x
)
,
f
(
a
)
,
s
=
t
,
,
Id
,
Inj(
A
;
B
;
f
)
,
(
x
l
)
,
namer-disjoint(
n1
;
n2
;
nmr1
;
nmr2
)
,
namer-shift(
n
;
namer
)
,
Namer(
n
;
Id_list
)
,
#$n
Lemmas
le
wf
origin
n, m:
, nmr:Namer(n+m;[]). namer-disjoint(n;m;nmr;namer-shift(n;nmr)) n, m:, nmr:Namer(n+m;[]). namer-disjoint(n;m;nmr;namer-shift(n;nmr)) 
Q
A
B j < k
}x:A. B(x)
B(x)
T
B(x)
l)